E, X1, X2:Type, info:(E(IdX1+(IdLnkE)X2)), pred?:(E(E+Unit)), e, e':E.
pred!(e;e')  Prop 

latex

Definitions	pred!(e;e'), P  Q, A, first(e), pred(e), A & B, Prop, b, rcv?(e), sender(e), x:A. B(x), P  Q, Unit, Id, IdLnk, t  T
Lemmas	IdLnk wf, Id wf, unit wf, sender wf, rcv? wf, assert wf, pred wf, first wf, not wf